A:Type, eq:EqDecider(A), df:x:A fp Type, f:x:A fp df(x)?Top, dg:x:A fp Type,
g:x:A fp dg(x)?Top.
df || dg
 (x:A. (x  dom(f))  (x  dom(df)))
 (x:A. (x  dom(g))  (x  dom(dg)))
 (f  g  x:A fp df  dg(x)?Top) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), x. t(x), a:A fp B(a), Top, f(x)?z, f || g, x  dom(f), b, P  Q, (x  l), f  g, deq-member(eq;x;L), b, filter(P;l), as @ bs, A, , , P & Q, P  Q, Unit, f(x), False, if b then t else f fi , P  Q, P  Q
Lemmas	member filter, member append, not functionality wrt iff, assert-deq-member, l member wf, fpf-join-dom, subtype rel self, fpf-join-ap, fpf-join wf, fpf-ap wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, not wf, append wf, filter wf, bnot wf, deq-member wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-compatible wf, fpf-cap wf, top wf, fpf wf, deq wf